Total termination of term rewriting
Identifieur interne : 00D163 ( Main/Exploration ); précédent : 00D162; suivant : 00D164Total termination of term rewriting
Auteurs : M. C. F. Ferreira [Pays-Bas] ; H. Zantema [Pays-Bas]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: We investigate proving termination of term rewriting systems by interpretation of terms in a compositional way in a total wellfounded order. This kind of termination is called total termination. On one hand it is more restrictive than simple termination, on the other it generalizes most of the usual techniques for proving termination. For total termination it turns out that below ε0 the only orders of interest are built from the natural numbers by lexicographic product and the multiset construction. By examples we show that both constructions are essential. For a wide class of term rewriting systems we prove that total termination is a modular property. Most of our techniques are based on ordinal arithmetic.
Url:
DOI: 10.1007/3-540-56868-9_17
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 000F04
- to stream Istex, to step Curation: 000E91
- to stream Istex, to step Checkpoint: 002E09
- to stream Main, to step Merge: 00DA35
- to stream Main, to step Curation: 00D163
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Total termination of term rewriting</title><author><name sortKey="Ferreira, M C F" sort="Ferreira, M C F" uniqKey="Ferreira M" first="M. C. F." last="Ferreira">M. C. F. Ferreira</name></author><author><name sortKey="Zantema, H" sort="Zantema, H" uniqKey="Zantema H" first="H." last="Zantema">H. Zantema</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:3FA616415E0FDA62714EDBE8F23B95524A56424A</idno><date when="1993" year="1993">1993</date><idno type="doi">10.1007/3-540-56868-9_17</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-4XJ63DPB-H/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">000F04</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">000F04</idno><idno type="wicri:Area/Istex/Curation">000E91</idno><idno type="wicri:Area/Istex/Checkpoint">002E09</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">002E09</idno><idno type="wicri:doubleKey">0302-9743:1993:Ferreira M:total:termination:of</idno><idno type="wicri:Area/Main/Merge">00DA35</idno><idno type="wicri:Area/Main/Curation">00D163</idno><idno type="wicri:Area/Main/Exploration">00D163</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Total termination of term rewriting</title><author><name sortKey="Ferreira, M C F" sort="Ferreira, M C F" uniqKey="Ferreira M" first="M. C. F." last="Ferreira">M. C. F. Ferreira</name><affiliation wicri:level="4"><country xml:lang="fr">Pays-Bas</country><wicri:regionArea>Department of Computer Science, Utrecht University, P.O. box 80.089, 3508, TB Utrecht</wicri:regionArea><orgName type="university">Université d'Utrecht</orgName><placeName><settlement type="city">Utrecht</settlement><region nuts="2">Utrecht (province)</region></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Pays-Bas</country></affiliation></author><author><name sortKey="Zantema, H" sort="Zantema, H" uniqKey="Zantema H" first="H." last="Zantema">H. Zantema</name><affiliation wicri:level="4"><country xml:lang="fr">Pays-Bas</country><wicri:regionArea>Department of Computer Science, Utrecht University, P.O. box 80.089, 3508, TB Utrecht</wicri:regionArea><orgName type="university">Université d'Utrecht</orgName><placeName><settlement type="city">Utrecht</settlement><region nuts="2">Utrecht (province)</region></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Pays-Bas</country></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><title level="s" type="abbrev">Lect Notes Comput Sci</title><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: We investigate proving termination of term rewriting systems by interpretation of terms in a compositional way in a total wellfounded order. This kind of termination is called total termination. On one hand it is more restrictive than simple termination, on the other it generalizes most of the usual techniques for proving termination. For total termination it turns out that below ε0 the only orders of interest are built from the natural numbers by lexicographic product and the multiset construction. By examples we show that both constructions are essential. For a wide class of term rewriting systems we prove that total termination is a modular property. Most of our techniques are based on ordinal arithmetic.</div></front></TEI><affiliations><list><country><li>Pays-Bas</li></country><region><li>Utrecht (province)</li></region><settlement><li>Utrecht</li></settlement><orgName><li>Université d'Utrecht</li></orgName></list><tree><country name="Pays-Bas"><region name="Utrecht (province)"><name sortKey="Ferreira, M C F" sort="Ferreira, M C F" uniqKey="Ferreira M" first="M. C. F." last="Ferreira">M. C. F. Ferreira</name></region><name sortKey="Ferreira, M C F" sort="Ferreira, M C F" uniqKey="Ferreira M" first="M. C. F." last="Ferreira">M. C. F. Ferreira</name><name sortKey="Zantema, H" sort="Zantema, H" uniqKey="Zantema H" first="H." last="Zantema">H. Zantema</name><name sortKey="Zantema, H" sort="Zantema, H" uniqKey="Zantema H" first="H." last="Zantema">H. Zantema</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 00D163 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 00D163 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:3FA616415E0FDA62714EDBE8F23B95524A56424A
|texte= Total termination of term rewriting
}}
| This area was generated with Dilib version V0.6.33. |  |